Nuprl Definition : es-interval
11,40
postcript
pdf
[
e
,
e'
] == filter((
ev
.es-ble{i:l}(
es
;
e
;
ev
)); append(before(
e'
); cons(
e'
; [])))
latex
clarification:
es-interval{i:l}
es-interval
(
es
;
e
;
e'
)
== filter((
ev
.es-ble{i:l}(
es
;
e
;
ev
)); append(es-before(
es
;
e'
); cons(
e'
; [])))
latex
Definitions
[
e
,
e'
]
,
filter(
P
;
l
)
,
es-ble{i:l}(
es
;
e
;
e'
)
,
append(
as
;
bs
)
,
before(
e
)
FDL editor aliases
es-interval
origin